COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(decl (x y z x1 x2 x3 y1 y2 y3 z1 z2 z3) |ground| variable sexp)
C00004 ENDMK
C⊗;
(decl (x y z x1 x2 x3 y1 y2 y3 z1 z2 z3) |ground| variable sexp)
(decl (a b c a1 a2 b1 b2 c1 c2) | ground| variable atom)
(decl (tt nnil) |ground | constant atom)
(decl (g g1 g2 g3) |ground| variable)
(decl (car cdr) |ground→ground| constant)
(decl (cons) |ground⊗ground →ground| constant)
(decl (phi) |ground→truthval| variable)
(axiom |∀g. atom(g)⊃sexp(g)|)
(axiom |∀x y.sexp(cons(x,y))|)
(axiom |∀g .sexp(g) ⊃ (atom(g) ∨ ∃x y. g=cons(x,y))|)
(axiom |∀x y. ¬atom(cons(x,y))|)
(axiom |∀x y.car(cons(x,y))=x|)
(axiom |∀x y.cdr(cons(x,y))=y|)
(axiom |∀phi.(∀a.phi(a) ∧ ∀x y.(phi(x)∧phi(y)⊃phi(cons(x,y))) ⊃∀ x.phi(x))|)
(decl (u v w u1 u2 u3 v1 v2 v3 w1 w2 w3) |ground| variable list)
(decl (null) |ground→truthval|)
(axiom |null(nnil)|)
(axiom |∀u.null(u)≡u=nnil|)
(axiom |list(nnil)|)
(axiom |∀g. list(g)⊃sexp(g)|)
(axiom |∀x u. ¬null(cons(x,u))|)